Nuprl Definition : ma-frame 11,40

M.frame(k affects x) == L != (M.2.2.2.2.2.2).1(x deq-member(KindDeq;k;L
latex



clarification:

M.frame(k affects x) == fpf-val(IdDeq; ((M.2.2.2.2.2.2).1); xx,L.(deq-member(KindDeq;k;L))) 
latex


Definitionsz != f(x P(a;z), IdDeq, t.1, t.2, b, deq-member(eq;x;L), KindDeq
FDL editor aliasesma-frame

origin